Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    f(j(x,y),y)  → g(f(x,k(y)))
2:    f(x,h1(y,z))  → h2(0,x,h1(y,z))
3:    g(h2(x,y,h1(z,u)))  → h2(s(x),y,h1(z,u))
4:    h2(x,j(y,h1(z,u)),h1(z,u))  → h2(s(x),y,h1(s(z),u))
5:    i(f(x,h(y)))  → y
6:    i(h2(s(x),y,h1(x,z)))  → z
7:    k(h(x))  → h1(0,x)
8:    k(h1(x,y))  → h1(s(x),y)
There are 6 dependency pairs:
9:    F(j(x,y),y)  → G(f(x,k(y)))
10:    F(j(x,y),y)  → F(x,k(y))
11:    F(j(x,y),y)  → K(y)
12:    F(x,h1(y,z))  → H2(0,x,h1(y,z))
13:    G(h2(x,y,h1(z,u)))  → H2(s(x),y,h1(z,u))
14:    H2(x,j(y,h1(z,u)),h1(z,u))  → H2(s(x),y,h1(s(z),u))
The approximated dependency graph contains 2 SCCs: {14} and {10}. Hence the TRS is terminating.
Tyrolean Termination Tool  (0.07 seconds)   ---  May 4, 2006